T:Type, d:EqDecider(T), x,y:T. (x = y)  ((eqof(d)(x,y))) 

latex

Definitions	x:A. B(x), EqDecider(T), P  Q, eqof(d), t.1, P  Q, P  Q, P  Q, t  T, prop{i:l}, x. t(x), x(s)
Lemmas	assert wf, pi1 wf, bool wf, iff wf